g:Mon. IsMonoid(|g|;*;e) & IsEqFun(|g|;=) 

latex

Up	groups 1
Definitions of Statement	IsMonoid(T;op;id), Mon
Definitions	t  T, x:A. B(x), True, T, , P & Q, Mon, IsMonoid(T;op;id), P  Q, SqStable(P)
Lemmas	mon wf, sq stable eqfun p, sq stable ident, sq stable assoc, grp eq wf, eqfun p wf, grp id wf, ident wf, grp op wf, grp car wf, assoc wf, sq stable and